$\forall$${\it es}$:ES, $m$:$\mathbb{N}^{+}$, $f$:(\{0..$m$$^{-}$\}$\rightarrow$E).
\\[0ex]($\forall$$i$:\{0..($m$ {-} 1)$^{-}$\}. ($f$($i$) $<$loc $f$($i$+1))) $\Rightarrow$ ($\forall$$i$:\{0..$m$$^{-}$\}, $j$:\{0..$i$$^{-}$\}. ($f$($j$) $<$loc $f$($i$)))